$\forall$$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $T$:Type, ${\it es}$:event\_system\{i:l\}.
\\[0ex]es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)
\\[0ex]$\Rightarrow$ subtype\_rel(es{-}vartype(${\it es}$; $i$; mkid\{ecl:ut2\}); $T$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$fpf{-}dom(id{-}deq; mkid\{ecl:ut2\}; ${\it ds}$)))
\\[0ex]$\Rightarrow$ es{-}decls(${\it es}$;$i$;fpf{-}join(id{-}deq; ${\it ds}$; fpf{-}single(mkid\{ecl:ut2\}; $T$));${\it da}$)